Issue4951b.agda:24,4-6
Cannot eliminate fibrant type Unitω
unless target type is also fibrant
when checking that the pattern tt has type Unitω
